E, X1, X2:Type, info:(E(IdX1+(IdLnkE)X2)), pred?:(E(E+Unit)).
WellFnd{i}(E;e,e'.first(e') & e = pred(e')  E)
 (e:E. first(e)  loc(pred(e)) = loc(e)  Id)
 (e, e':E. loc(e) = loc(e')  Id  pred?(e) = pred?(e')  e = e')
 (e, e':E.
 (loc(e) = loc(e')  Id
 ( (e e,e'. first(e') & e = pred(e')^+ e')
 (  e = e'
 (  (e' e,e'. first(e') & e = pred(e')^+ e)) 

latex

Definitions

Trans x,y:T. E(x;y), , P  Q, P & Q, , b, SQType(T), R^+, True, , x:A. B(x), , AB, rel_exp(T;R;n), i=j, x f y, x. t(x), {T}, Dec(P), P  Q, False, x:A. B(x), P  Q, Id, loc(e), R^*, A & B, A, b, first(e), pred(e), IdLnk, WellFnd{i}(A;x,y.R(x;y)), x,y. t(x;y), Unit, t  T, Prop

Lemmas

unit wf, loc wf, Id wf, pred wf, first wf, assert wf, not wf, wellfounded wf, IdLnk wf, decidable assert, rel star wf, rel exp wf, le wf, it wf, true wf, false wf, rel rel star, rel star transitivity, rel plus wf, decidable int equal, bnot wf, bool wf, eq int wf, assert of eq int, not functionality wrt iff, assert of bnot, iff transitivity, eqff to assert, bool sq, eqtt to assert, bool cases, nat plus inc, rel-rel-plus, rel plus trans